ma-interface-consistent-at(es;i;X)
== let ds,F = X(i)
== in
== k:{k:Knd| hasloc(k;i)} .
== (k  dom(F))
==  (e@i. (kind(e) = k)  (valtype(e) r (F(k).1)) & (x:Id. vartype(i;x) r ds(x)?Top)) 

latex

---

clarification:

ma-interface-consistent-at(es;i;X)
== let ds,F = XIdDeq(i)
== in
== k:{k:Knd| hasloc(k;i)} .
== (fpf-dom(KindDeq; k; F))
==  (alle-at(es;i;e.(es-kind(es; e) = k  Knd)  (es-valtype(es; e) r (FKindDeq(k).1)))
==  & (x:Id. es-vartype(es; i; x) r fpf-cap(ds;IdDeq;x;Top))) 

latex

Definitions	let x,y = A in B(x;y), {x:A| B(x)} , hasloc(k;i), b, x  dom(f), P & Q, e@i. P(e), P  Q, s = t, Knd, kind(e), valtype(e), t.1, f(x), KindDeq, x:A. B(x), Id, vartype(i;x), f(x)?z, IdDeq, Top
FDL editor aliases	ma-interface-consistent-at